Automating inversion of inductive predicates in Coq
Identifieur interne : 002990 ( Istex/Checkpoint ); précédent : 002989; suivant : 002991Automating inversion of inductive predicates in Coq
Auteurs : Cristina Cornes [France] ; Delphine Terrasse [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: An inductive definition of a set is often informally presented by giving some rules that explain how to build the elements of the set. The closure property states that any object is in the set if and only if it has been generated according to the formation rules. This is enough to justify case analysis reasoning: we can read the formation rules backwards to derive the necessary conditions for a given instance to hold. The problem of inversion consists in finding out these conditions. In this paper we address the problem of deriving inversion lemmas in logical frameworks based on Type Theory that have been extended with inductive definitions at the primitive level. These frameworks associate to each inductive definition a case analysis principle corresponding to the closure property. In this formal context, inversion lemmas can be seen as derived case analysis principles. Though they are intuitively simple they are curiously hard to formalize. We relate first inversion to completion in logic programming. Then we discuss two general algorithms to generate inversion lemmas. They are presented in the proof assistant system Coq [8] but they can be adapted to any other proof assistant having a similar notion of inductive definition.
Url:
DOI: 10.1007/3-540-61780-9_64
Affiliations:
Links toward previous steps (curation, corpus...)
Links to Exploration step
ISTEX:B14A35D0F368A46B5BE79CAED0C35EF10384457ELe document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Automating inversion of inductive predicates in Coq</title><author><name sortKey="Cornes, Cristina" sort="Cornes, Cristina" uniqKey="Cornes C" first="Cristina" last="Cornes">Cristina Cornes</name></author><author><name sortKey="Terrasse, Delphine" sort="Terrasse, Delphine" uniqKey="Terrasse D" first="Delphine" last="Terrasse">Delphine Terrasse</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:B14A35D0F368A46B5BE79CAED0C35EF10384457E</idno><date when="1996" year="1996">1996</date><idno type="doi">10.1007/3-540-61780-9_64</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-VC3KRWKT-Q/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">002A04</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002A04</idno><idno type="wicri:Area/Istex/Curation">002967</idno><idno type="wicri:Area/Istex/Checkpoint">002990</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">002990</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Automating inversion of inductive predicates in Coq</title><author><name sortKey="Cornes, Cristina" sort="Cornes, Cristina" uniqKey="Cornes C" first="Cristina" last="Cornes">Cristina Cornes</name><affiliation wicri:level="1"><country xml:lang="fr">France</country><wicri:regionArea>INRIA Rocquencourt, B.P. 105, 78153, Le Chesnay, Cedex</wicri:regionArea><wicri:noRegion>Cedex</wicri:noRegion><wicri:noRegion>Cedex</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author><author><name sortKey="Terrasse, Delphine" sort="Terrasse, Delphine" uniqKey="Terrasse D" first="Delphine" last="Terrasse">Delphine Terrasse</name><affiliation wicri:level="1"><country xml:lang="fr">France</country><wicri:regionArea>INRIA Sophia-Antipolis, 2004 route des Lucioles, BP 93, Sophia Antipolis Cedex</wicri:regionArea><wicri:noRegion>Sophia Antipolis Cedex</wicri:noRegion><wicri:noRegion>Sophia Antipolis Cedex</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><title level="s" type="abbrev">Lect Notes Comput Sci</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: An inductive definition of a set is often informally presented by giving some rules that explain how to build the elements of the set. The closure property states that any object is in the set if and only if it has been generated according to the formation rules. This is enough to justify case analysis reasoning: we can read the formation rules backwards to derive the necessary conditions for a given instance to hold. The problem of inversion consists in finding out these conditions. In this paper we address the problem of deriving inversion lemmas in logical frameworks based on Type Theory that have been extended with inductive definitions at the primitive level. These frameworks associate to each inductive definition a case analysis principle corresponding to the closure property. In this formal context, inversion lemmas can be seen as derived case analysis principles. Though they are intuitively simple they are curiously hard to formalize. We relate first inversion to completion in logic programming. Then we discuss two general algorithms to generate inversion lemmas. They are presented in the proof assistant system Coq [8] but they can be adapted to any other proof assistant having a similar notion of inductive definition.</div></front></TEI><affiliations><list><country><li>France</li></country></list><tree><country name="France"><noRegion><name sortKey="Cornes, Cristina" sort="Cornes, Cristina" uniqKey="Cornes C" first="Cristina" last="Cornes">Cristina Cornes</name></noRegion><name sortKey="Cornes, Cristina" sort="Cornes, Cristina" uniqKey="Cornes C" first="Cristina" last="Cornes">Cristina Cornes</name><name sortKey="Terrasse, Delphine" sort="Terrasse, Delphine" uniqKey="Terrasse D" first="Delphine" last="Terrasse">Delphine Terrasse</name><name sortKey="Terrasse, Delphine" sort="Terrasse, Delphine" uniqKey="Terrasse D" first="Delphine" last="Terrasse">Delphine Terrasse</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Checkpoint
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002990 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Checkpoint/biblio.hfd -nk 002990 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Checkpoint
|type= RBID
|clé= ISTEX:B14A35D0F368A46B5BE79CAED0C35EF10384457E
|texte= Automating inversion of inductive predicates in Coq
}}
| This area was generated with Dilib version V0.6.33. |  |